Calculus of explicit substitutions is a λ-calculus in which substitution is not external but is fully integrated at the same level as β~reduction. This internalisation of the substitution calculus is achieved by rewrite rules which allow a full and easy mechanism for describing β~reduction. The original goal of explicit substitutions is to provide the implementor of {\sc Automath} (and later of functional programming languages) with a finer granularity in the description of the process of substitutions, as substitutions play the central role in the implementation of those systems and languages. This way, controls that postpone costly operations may be adopted and operations that will turn out to be unnecessary will never be performed {\it (lazy evaluation)\/}. Except for a sketched attempt by Abadai, Cardelli, Curien and Levy, ({\it λσ-calculus with names\/}), all the proposed calculi use {\it De Bruijn indices\/}. That notation has two drawbacks. First, terms are hard to read due to the use of numbers instead of names and due to the fact that the ``same'' variable is designated by different numbers according to the context. Second the association between variables and their values, the so-called environment, keeps changing whenever one leaves or enters an abstraction. To our knowledge ``levels'' were only mentioned twice in the literature, first by de Bruijn and later by Crégut in his PhD, but never in the framework of explicit substitutions. Both authors suggest a canonical indexing of the variables ; Crégut calls it ``reversed De Bruijn indexing''. To make formulas as readable as in the classical λ-calculus, we give each variable a name made from its index and that name is the same everywhere in a pure term, i.e., a term without {\it closure\/} (see below) unlike classical De Bruijn index. Two important features of λ\chi are the absence of variables of type {\it substitution\/} and the absence of composition of substitutions. Of course, the λ-calculus describes variables, but they are seen as constants by the rewrite system λ\chi and they will be called {\it names\/} in what follows. The only variables of λ\chi (those which play an actual role in the rewrite system) are of type {\sl Term\/} and of type {\sl Nat\/}.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00C374 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00C374 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     CRIN:lescanne95b
   |texte=   Explicit Substitutions with de Bruijn's Levels
}}